H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 4.7780000000000005 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ BR

mainModule Main

((digitToInt :: Char -> Int) :: Char -> Int)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule Main

((digitToInt :: Char -> Int) :: Char -> Int)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

The following Function with conditions

digitToInt c

| isDigit c

= fromEnum c - fromEnum '0'

| c >= 'a' && c <= 'f'

= fromEnum c - fromEnum 'a' + 10

| c >= 'A' && c <= 'F'

= fromEnum c - fromEnum 'A' + 10

| otherwise

= error []

is transformed to

digitToInt c = digitToInt4 c

digitToInt0 c True = error []

digitToInt1 c True = fromEnum c - fromEnum 'A' + 10

digitToInt1 c False = digitToInt0 c otherwise

digitToInt3 c True = fromEnum c - fromEnum '0'

digitToInt3 c False = digitToInt2 c (c >= 'a' && c <= 'f')

digitToInt2 c True = fromEnum c - fromEnum 'a' + 10

digitToInt2 c False = digitToInt1 c (c >= 'A' && c <= 'F')

digitToInt4 c = digitToInt3 c (isDigit c)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

mainModule Main

((digitToInt :: Char -> Int) :: Char -> Int)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

mainModule Main

(digitToInt :: Char -> Int)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="digitToInt",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="digitToInt vx3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="digitToInt4 vx3",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="digitToInt3 vx3 (isDigit vx3)",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6 -> 10[label="",style="dashed", color="red", weight=0];
6[label="digitToInt3 vx3 (vx3 >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))) && vx3 <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];6 -> 11[label="",style="dashed", color="magenta", weight=3];
6 -> 12[label="",style="dashed", color="magenta", weight=3];
6 -> 13[label="",style="dashed", color="magenta", weight=3];
11[label="vx3",fontsize=16,color="green",shape="box"];12[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];13[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];10[label="digitToInt3 vx8 (vx8 >= Char (Succ vx9) && vx8 <= Char (Succ vx10))",fontsize=16,color="black",shape="triangle"];10 -> 17[label="",style="solid", color="black", weight=3];
17[label="digitToInt3 vx8 (compare vx8 (Char (Succ vx9)) /= LT && vx8 <= Char (Succ vx10))",fontsize=16,color="black",shape="box"];17 -> 18[label="",style="solid", color="black", weight=3];
18[label="digitToInt3 vx8 (not (compare vx8 (Char (Succ vx9)) == LT) && vx8 <= Char (Succ vx10))",fontsize=16,color="black",shape="box"];18 -> 19[label="",style="solid", color="black", weight=3];
19[label="digitToInt3 vx8 (not (primCmpChar vx8 (Char (Succ vx9)) == LT) && vx8 <= Char (Succ vx10))",fontsize=16,color="burlywood",shape="box"];1269[label="vx8/Char vx80",fontsize=10,color="white",style="solid",shape="box"];19 -> 1269[label="",style="solid", color="burlywood", weight=9];
1269 -> 20[label="",style="solid", color="burlywood", weight=3];
20[label="digitToInt3 (Char vx80) (not (primCmpChar (Char vx80) (Char (Succ vx9)) == LT) && Char vx80 <= Char (Succ vx10))",fontsize=16,color="black",shape="box"];20 -> 21[label="",style="solid", color="black", weight=3];
21[label="digitToInt3 (Char vx80) (not (primCmpNat vx80 (Succ vx9) == LT) && Char vx80 <= Char (Succ vx10))",fontsize=16,color="burlywood",shape="box"];1270[label="vx80/Succ vx800",fontsize=10,color="white",style="solid",shape="box"];21 -> 1270[label="",style="solid", color="burlywood", weight=9];
1270 -> 22[label="",style="solid", color="burlywood", weight=3];
1271[label="vx80/Zero",fontsize=10,color="white",style="solid",shape="box"];21 -> 1271[label="",style="solid", color="burlywood", weight=9];
1271 -> 23[label="",style="solid", color="burlywood", weight=3];
22[label="digitToInt3 (Char (Succ vx800)) (not (primCmpNat (Succ vx800) (Succ vx9) == LT) && Char (Succ vx800) <= Char (Succ vx10))",fontsize=16,color="black",shape="box"];22 -> 24[label="",style="solid", color="black", weight=3];
23[label="digitToInt3 (Char Zero) (not (primCmpNat Zero (Succ vx9) == LT) && Char Zero <= Char (Succ vx10))",fontsize=16,color="black",shape="box"];23 -> 25[label="",style="solid", color="black", weight=3];
24 -> 328[label="",style="dashed", color="red", weight=0];
24[label="digitToInt3 (Char (Succ vx800)) (not (primCmpNat vx800 vx9 == LT) && Char (Succ vx800) <= Char (Succ vx10))",fontsize=16,color="magenta"];24 -> 329[label="",style="dashed", color="magenta", weight=3];
24 -> 330[label="",style="dashed", color="magenta", weight=3];
24 -> 331[label="",style="dashed", color="magenta", weight=3];
24 -> 332[label="",style="dashed", color="magenta", weight=3];
25[label="digitToInt3 (Char Zero) (not (LT == LT) && Char Zero <= Char (Succ vx10))",fontsize=16,color="black",shape="box"];25 -> 28[label="",style="solid", color="black", weight=3];
329[label="vx800",fontsize=16,color="green",shape="box"];330[label="vx800",fontsize=16,color="green",shape="box"];331[label="vx10",fontsize=16,color="green",shape="box"];332[label="vx9",fontsize=16,color="green",shape="box"];328[label="digitToInt3 (Char (Succ vx61)) (not (primCmpNat vx62 vx63 == LT) && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="burlywood",shape="triangle"];1273[label="vx62/Succ vx620",fontsize=10,color="white",style="solid",shape="box"];328 -> 1273[label="",style="solid", color="burlywood", weight=9];
1273 -> 361[label="",style="solid", color="burlywood", weight=3];
1274[label="vx62/Zero",fontsize=10,color="white",style="solid",shape="box"];328 -> 1274[label="",style="solid", color="burlywood", weight=9];
1274 -> 362[label="",style="solid", color="burlywood", weight=3];
28[label="digitToInt3 (Char Zero) (not True && Char Zero <= Char (Succ vx10))",fontsize=16,color="black",shape="box"];28 -> 33[label="",style="solid", color="black", weight=3];
361[label="digitToInt3 (Char (Succ vx61)) (not (primCmpNat (Succ vx620) vx63 == LT) && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="burlywood",shape="box"];1275[label="vx63/Succ vx630",fontsize=10,color="white",style="solid",shape="box"];361 -> 1275[label="",style="solid", color="burlywood", weight=9];
1275 -> 364[label="",style="solid", color="burlywood", weight=3];
1276[label="vx63/Zero",fontsize=10,color="white",style="solid",shape="box"];361 -> 1276[label="",style="solid", color="burlywood", weight=9];
1276 -> 365[label="",style="solid", color="burlywood", weight=3];
362[label="digitToInt3 (Char (Succ vx61)) (not (primCmpNat Zero vx63 == LT) && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="burlywood",shape="box"];1277[label="vx63/Succ vx630",fontsize=10,color="white",style="solid",shape="box"];362 -> 1277[label="",style="solid", color="burlywood", weight=9];
1277 -> 366[label="",style="solid", color="burlywood", weight=3];
1278[label="vx63/Zero",fontsize=10,color="white",style="solid",shape="box"];362 -> 1278[label="",style="solid", color="burlywood", weight=9];
1278 -> 367[label="",style="solid", color="burlywood", weight=3];
33[label="digitToInt3 (Char Zero) (False && Char Zero <= Char (Succ vx10))",fontsize=16,color="black",shape="box"];33 -> 38[label="",style="solid", color="black", weight=3];
364[label="digitToInt3 (Char (Succ vx61)) (not (primCmpNat (Succ vx620) (Succ vx630) == LT) && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="black",shape="box"];364 -> 369[label="",style="solid", color="black", weight=3];
365[label="digitToInt3 (Char (Succ vx61)) (not (primCmpNat (Succ vx620) Zero == LT) && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="black",shape="box"];365 -> 370[label="",style="solid", color="black", weight=3];
366[label="digitToInt3 (Char (Succ vx61)) (not (primCmpNat Zero (Succ vx630) == LT) && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="black",shape="box"];366 -> 371[label="",style="solid", color="black", weight=3];
367[label="digitToInt3 (Char (Succ vx61)) (not (primCmpNat Zero Zero == LT) && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="black",shape="box"];367 -> 372[label="",style="solid", color="black", weight=3];
38[label="digitToInt3 (Char Zero) False",fontsize=16,color="black",shape="box"];38 -> 44[label="",style="solid", color="black", weight=3];
369 -> 328[label="",style="dashed", color="red", weight=0];
369[label="digitToInt3 (Char (Succ vx61)) (not (primCmpNat vx620 vx630 == LT) && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="magenta"];369 -> 374[label="",style="dashed", color="magenta", weight=3];
369 -> 375[label="",style="dashed", color="magenta", weight=3];
370[label="digitToInt3 (Char (Succ vx61)) (not (GT == LT) && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="black",shape="box"];370 -> 376[label="",style="solid", color="black", weight=3];
371[label="digitToInt3 (Char (Succ vx61)) (not (LT == LT) && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="black",shape="box"];371 -> 377[label="",style="solid", color="black", weight=3];
372[label="digitToInt3 (Char (Succ vx61)) (not (EQ == LT) && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="black",shape="box"];372 -> 378[label="",style="solid", color="black", weight=3];
44 -> 61[label="",style="dashed", color="red", weight=0];
44[label="digitToInt2 (Char Zero) (Char Zero >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && Char Zero <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];44 -> 62[label="",style="dashed", color="magenta", weight=3];
44 -> 63[label="",style="dashed", color="magenta", weight=3];
374[label="vx620",fontsize=16,color="green",shape="box"];375[label="vx630",fontsize=16,color="green",shape="box"];376[label="digitToInt3 (Char (Succ vx61)) (not False && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="black",shape="triangle"];376 -> 380[label="",style="solid", color="black", weight=3];
377[label="digitToInt3 (Char (Succ vx61)) (not True && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="black",shape="box"];377 -> 381[label="",style="solid", color="black", weight=3];
378 -> 376[label="",style="dashed", color="red", weight=0];
378[label="digitToInt3 (Char (Succ vx61)) (not False && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="magenta"];62[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];63[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];61[label="digitToInt2 (Char Zero) (Char Zero >= Char (Succ vx14) && Char Zero <= Char (Succ vx15))",fontsize=16,color="black",shape="triangle"];61 -> 66[label="",style="solid", color="black", weight=3];
380[label="digitToInt3 (Char (Succ vx61)) (True && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="black",shape="box"];380 -> 383[label="",style="solid", color="black", weight=3];
381[label="digitToInt3 (Char (Succ vx61)) (False && Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="black",shape="box"];381 -> 384[label="",style="solid", color="black", weight=3];
66[label="digitToInt2 (Char Zero) (compare (Char Zero) (Char (Succ vx14)) /= LT && Char Zero <= Char (Succ vx15))",fontsize=16,color="black",shape="box"];66 -> 75[label="",style="solid", color="black", weight=3];
383[label="digitToInt3 (Char (Succ vx61)) (Char (Succ vx61) <= Char (Succ vx64))",fontsize=16,color="black",shape="box"];383 -> 386[label="",style="solid", color="black", weight=3];
384[label="digitToInt3 (Char (Succ vx61)) False",fontsize=16,color="black",shape="triangle"];384 -> 387[label="",style="solid", color="black", weight=3];
75[label="digitToInt2 (Char Zero) (not (compare (Char Zero) (Char (Succ vx14)) == LT) && Char Zero <= Char (Succ vx15))",fontsize=16,color="black",shape="box"];75 -> 86[label="",style="solid", color="black", weight=3];
386[label="digitToInt3 (Char (Succ vx61)) (compare (Char (Succ vx61)) (Char (Succ vx64)) /= GT)",fontsize=16,color="black",shape="box"];386 -> 388[label="",style="solid", color="black", weight=3];
387 -> 393[label="",style="dashed", color="red", weight=0];
387[label="digitToInt2 (Char (Succ vx61)) (Char (Succ vx61) >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && Char (Succ vx61) <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];387 -> 394[label="",style="dashed", color="magenta", weight=3];
387 -> 395[label="",style="dashed", color="magenta", weight=3];
387 -> 396[label="",style="dashed", color="magenta", weight=3];
86[label="digitToInt2 (Char Zero) (not (primCmpChar (Char Zero) (Char (Succ vx14)) == LT) && Char Zero <= Char (Succ vx15))",fontsize=16,color="black",shape="box"];86 -> 100[label="",style="solid", color="black", weight=3];
388[label="digitToInt3 (Char (Succ vx61)) (not (compare (Char (Succ vx61)) (Char (Succ vx64)) == GT))",fontsize=16,color="black",shape="box"];388 -> 392[label="",style="solid", color="black", weight=3];
394[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];395[label="vx61",fontsize=16,color="green",shape="box"];396[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];393[label="digitToInt2 (Char (Succ vx69)) (Char (Succ vx69) >= Char (Succ vx70) && Char (Succ vx69) <= Char (Succ vx71))",fontsize=16,color="black",shape="triangle"];393 -> 400[label="",style="solid", color="black", weight=3];
100[label="digitToInt2 (Char Zero) (not (primCmpNat Zero (Succ vx14) == LT) && Char Zero <= Char (Succ vx15))",fontsize=16,color="black",shape="box"];100 -> 110[label="",style="solid", color="black", weight=3];
392[label="digitToInt3 (Char (Succ vx61)) (not (primCmpChar (Char (Succ vx61)) (Char (Succ vx64)) == GT))",fontsize=16,color="black",shape="box"];392 -> 401[label="",style="solid", color="black", weight=3];
400[label="digitToInt2 (Char (Succ vx69)) (compare (Char (Succ vx69)) (Char (Succ vx70)) /= LT && Char (Succ vx69) <= Char (Succ vx71))",fontsize=16,color="black",shape="box"];400 -> 402[label="",style="solid", color="black", weight=3];
110[label="digitToInt2 (Char Zero) (not (LT == LT) && Char Zero <= Char (Succ vx15))",fontsize=16,color="black",shape="box"];110 -> 122[label="",style="solid", color="black", weight=3];
401 -> 609[label="",style="dashed", color="red", weight=0];
401[label="digitToInt3 (Char (Succ vx61)) (not (primCmpNat (Succ vx61) (Succ vx64) == GT))",fontsize=16,color="magenta"];401 -> 610[label="",style="dashed", color="magenta", weight=3];
401 -> 611[label="",style="dashed", color="magenta", weight=3];
401 -> 612[label="",style="dashed", color="magenta", weight=3];
402[label="digitToInt2 (Char (Succ vx69)) (not (compare (Char (Succ vx69)) (Char (Succ vx70)) == LT) && Char (Succ vx69) <= Char (Succ vx71))",fontsize=16,color="black",shape="box"];402 -> 404[label="",style="solid", color="black", weight=3];
122[label="digitToInt2 (Char Zero) (not True && Char Zero <= Char (Succ vx15))",fontsize=16,color="black",shape="box"];122 -> 139[label="",style="solid", color="black", weight=3];
610[label="Succ vx61",fontsize=16,color="green",shape="box"];611[label="vx61",fontsize=16,color="green",shape="box"];612[label="Succ vx64",fontsize=16,color="green",shape="box"];609[label="digitToInt3 (Char (Succ vx89)) (not (primCmpNat vx90 vx91 == GT))",fontsize=16,color="burlywood",shape="triangle"];1284[label="vx90/Succ vx900",fontsize=10,color="white",style="solid",shape="box"];609 -> 1284[label="",style="solid", color="burlywood", weight=9];
1284 -> 631[label="",style="solid", color="burlywood", weight=3];
1285[label="vx90/Zero",fontsize=10,color="white",style="solid",shape="box"];609 -> 1285[label="",style="solid", color="burlywood", weight=9];
1285 -> 632[label="",style="solid", color="burlywood", weight=3];
404[label="digitToInt2 (Char (Succ vx69)) (not (primCmpChar (Char (Succ vx69)) (Char (Succ vx70)) == LT) && Char (Succ vx69) <= Char (Succ vx71))",fontsize=16,color="black",shape="box"];404 -> 407[label="",style="solid", color="black", weight=3];
139[label="digitToInt2 (Char Zero) (False && Char Zero <= Char (Succ vx15))",fontsize=16,color="black",shape="box"];139 -> 152[label="",style="solid", color="black", weight=3];
631[label="digitToInt3 (Char (Succ vx89)) (not (primCmpNat (Succ vx900) vx91 == GT))",fontsize=16,color="burlywood",shape="box"];1286[label="vx91/Succ vx910",fontsize=10,color="white",style="solid",shape="box"];631 -> 1286[label="",style="solid", color="burlywood", weight=9];
1286 -> 641[label="",style="solid", color="burlywood", weight=3];
1287[label="vx91/Zero",fontsize=10,color="white",style="solid",shape="box"];631 -> 1287[label="",style="solid", color="burlywood", weight=9];
1287 -> 642[label="",style="solid", color="burlywood", weight=3];
632[label="digitToInt3 (Char (Succ vx89)) (not (primCmpNat Zero vx91 == GT))",fontsize=16,color="burlywood",shape="box"];1288[label="vx91/Succ vx910",fontsize=10,color="white",style="solid",shape="box"];632 -> 1288[label="",style="solid", color="burlywood", weight=9];
1288 -> 643[label="",style="solid", color="burlywood", weight=3];
1289[label="vx91/Zero",fontsize=10,color="white",style="solid",shape="box"];632 -> 1289[label="",style="solid", color="burlywood", weight=9];
1289 -> 644[label="",style="solid", color="burlywood", weight=3];
407 -> 677[label="",style="dashed", color="red", weight=0];
407[label="digitToInt2 (Char (Succ vx69)) (not (primCmpNat (Succ vx69) (Succ vx70) == LT) && Char (Succ vx69) <= Char (Succ vx71))",fontsize=16,color="magenta"];407 -> 678[label="",style="dashed", color="magenta", weight=3];
407 -> 679[label="",style="dashed", color="magenta", weight=3];
407 -> 680[label="",style="dashed", color="magenta", weight=3];
407 -> 681[label="",style="dashed", color="magenta", weight=3];
152[label="digitToInt2 (Char Zero) False",fontsize=16,color="black",shape="box"];152 -> 169[label="",style="solid", color="black", weight=3];
641[label="digitToInt3 (Char (Succ vx89)) (not (primCmpNat (Succ vx900) (Succ vx910) == GT))",fontsize=16,color="black",shape="box"];641 -> 663[label="",style="solid", color="black", weight=3];
642[label="digitToInt3 (Char (Succ vx89)) (not (primCmpNat (Succ vx900) Zero == GT))",fontsize=16,color="black",shape="box"];642 -> 664[label="",style="solid", color="black", weight=3];
643[label="digitToInt3 (Char (Succ vx89)) (not (primCmpNat Zero (Succ vx910) == GT))",fontsize=16,color="black",shape="box"];643 -> 665[label="",style="solid", color="black", weight=3];
644[label="digitToInt3 (Char (Succ vx89)) (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];644 -> 666[label="",style="solid", color="black", weight=3];
678[label="Succ vx70",fontsize=16,color="green",shape="box"];679[label="vx69",fontsize=16,color="green",shape="box"];680[label="vx71",fontsize=16,color="green",shape="box"];681[label="Succ vx69",fontsize=16,color="green",shape="box"];677[label="digitToInt2 (Char (Succ vx98)) (not (primCmpNat vx99 vx100 == LT) && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="burlywood",shape="triangle"];1291[label="vx99/Succ vx990",fontsize=10,color="white",style="solid",shape="box"];677 -> 1291[label="",style="solid", color="burlywood", weight=9];
1291 -> 706[label="",style="solid", color="burlywood", weight=3];
1292[label="vx99/Zero",fontsize=10,color="white",style="solid",shape="box"];677 -> 1292[label="",style="solid", color="burlywood", weight=9];
1292 -> 707[label="",style="solid", color="burlywood", weight=3];
169 -> 214[label="",style="dashed", color="red", weight=0];
169[label="digitToInt1 (Char Zero) (Char Zero >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && Char Zero <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];169 -> 215[label="",style="dashed", color="magenta", weight=3];
169 -> 216[label="",style="dashed", color="magenta", weight=3];
663 -> 609[label="",style="dashed", color="red", weight=0];
663[label="digitToInt3 (Char (Succ vx89)) (not (primCmpNat vx900 vx910 == GT))",fontsize=16,color="magenta"];663 -> 708[label="",style="dashed", color="magenta", weight=3];
663 -> 709[label="",style="dashed", color="magenta", weight=3];
664[label="digitToInt3 (Char (Succ vx89)) (not (GT == GT))",fontsize=16,color="black",shape="box"];664 -> 710[label="",style="solid", color="black", weight=3];
665[label="digitToInt3 (Char (Succ vx89)) (not (LT == GT))",fontsize=16,color="black",shape="box"];665 -> 711[label="",style="solid", color="black", weight=3];
666[label="digitToInt3 (Char (Succ vx89)) (not (EQ == GT))",fontsize=16,color="black",shape="box"];666 -> 712[label="",style="solid", color="black", weight=3];
706[label="digitToInt2 (Char (Succ vx98)) (not (primCmpNat (Succ vx990) vx100 == LT) && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="burlywood",shape="box"];1295[label="vx100/Succ vx1000",fontsize=10,color="white",style="solid",shape="box"];706 -> 1295[label="",style="solid", color="burlywood", weight=9];
1295 -> 713[label="",style="solid", color="burlywood", weight=3];
1296[label="vx100/Zero",fontsize=10,color="white",style="solid",shape="box"];706 -> 1296[label="",style="solid", color="burlywood", weight=9];
1296 -> 714[label="",style="solid", color="burlywood", weight=3];
707[label="digitToInt2 (Char (Succ vx98)) (not (primCmpNat Zero vx100 == LT) && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="burlywood",shape="box"];1297[label="vx100/Succ vx1000",fontsize=10,color="white",style="solid",shape="box"];707 -> 1297[label="",style="solid", color="burlywood", weight=9];
1297 -> 715[label="",style="solid", color="burlywood", weight=3];
1298[label="vx100/Zero",fontsize=10,color="white",style="solid",shape="box"];707 -> 1298[label="",style="solid", color="burlywood", weight=9];
1298 -> 716[label="",style="solid", color="burlywood", weight=3];
215[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];216[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];214[label="digitToInt1 (Char Zero) (Char Zero >= Char (Succ vx37) && Char Zero <= Char (Succ vx38))",fontsize=16,color="black",shape="triangle"];214 -> 220[label="",style="solid", color="black", weight=3];
708[label="vx900",fontsize=16,color="green",shape="box"];709[label="vx910",fontsize=16,color="green",shape="box"];710[label="digitToInt3 (Char (Succ vx89)) (not True)",fontsize=16,color="black",shape="box"];710 -> 717[label="",style="solid", color="black", weight=3];
711[label="digitToInt3 (Char (Succ vx89)) (not False)",fontsize=16,color="black",shape="triangle"];711 -> 718[label="",style="solid", color="black", weight=3];
712 -> 711[label="",style="dashed", color="red", weight=0];
712[label="digitToInt3 (Char (Succ vx89)) (not False)",fontsize=16,color="magenta"];713[label="digitToInt2 (Char (Succ vx98)) (not (primCmpNat (Succ vx990) (Succ vx1000) == LT) && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="black",shape="box"];713 -> 719[label="",style="solid", color="black", weight=3];
714[label="digitToInt2 (Char (Succ vx98)) (not (primCmpNat (Succ vx990) Zero == LT) && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="black",shape="box"];714 -> 720[label="",style="solid", color="black", weight=3];
715[label="digitToInt2 (Char (Succ vx98)) (not (primCmpNat Zero (Succ vx1000) == LT) && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="black",shape="box"];715 -> 721[label="",style="solid", color="black", weight=3];
716[label="digitToInt2 (Char (Succ vx98)) (not (primCmpNat Zero Zero == LT) && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="black",shape="box"];716 -> 722[label="",style="solid", color="black", weight=3];
220[label="digitToInt1 (Char Zero) (compare (Char Zero) (Char (Succ vx37)) /= LT && Char Zero <= Char (Succ vx38))",fontsize=16,color="black",shape="box"];220 -> 238[label="",style="solid", color="black", weight=3];
717 -> 384[label="",style="dashed", color="red", weight=0];
717[label="digitToInt3 (Char (Succ vx89)) False",fontsize=16,color="magenta"];717 -> 723[label="",style="dashed", color="magenta", weight=3];
718[label="digitToInt3 (Char (Succ vx89)) True",fontsize=16,color="black",shape="box"];718 -> 724[label="",style="solid", color="black", weight=3];
719 -> 677[label="",style="dashed", color="red", weight=0];
719[label="digitToInt2 (Char (Succ vx98)) (not (primCmpNat vx990 vx1000 == LT) && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="magenta"];719 -> 725[label="",style="dashed", color="magenta", weight=3];
719 -> 726[label="",style="dashed", color="magenta", weight=3];
720[label="digitToInt2 (Char (Succ vx98)) (not (GT == LT) && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="black",shape="box"];720 -> 727[label="",style="solid", color="black", weight=3];
721[label="digitToInt2 (Char (Succ vx98)) (not (LT == LT) && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="black",shape="box"];721 -> 728[label="",style="solid", color="black", weight=3];
722[label="digitToInt2 (Char (Succ vx98)) (not (EQ == LT) && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="black",shape="box"];722 -> 729[label="",style="solid", color="black", weight=3];
238[label="digitToInt1 (Char Zero) (not (compare (Char Zero) (Char (Succ vx37)) == LT) && Char Zero <= Char (Succ vx38))",fontsize=16,color="black",shape="box"];238 -> 272[label="",style="solid", color="black", weight=3];
723[label="vx89",fontsize=16,color="green",shape="box"];724 -> 730[label="",style="dashed", color="red", weight=0];
724[label="fromEnum (Char (Succ vx89)) - fromEnum (Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];724 -> 731[label="",style="dashed", color="magenta", weight=3];
724 -> 732[label="",style="dashed", color="magenta", weight=3];
725[label="vx1000",fontsize=16,color="green",shape="box"];726[label="vx990",fontsize=16,color="green",shape="box"];727[label="digitToInt2 (Char (Succ vx98)) (not False && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="black",shape="triangle"];727 -> 733[label="",style="solid", color="black", weight=3];
728[label="digitToInt2 (Char (Succ vx98)) (not True && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="black",shape="box"];728 -> 734[label="",style="solid", color="black", weight=3];
729 -> 727[label="",style="dashed", color="red", weight=0];
729[label="digitToInt2 (Char (Succ vx98)) (not False && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="magenta"];272[label="digitToInt1 (Char Zero) (not (primCmpChar (Char Zero) (Char (Succ vx37)) == LT) && Char Zero <= Char (Succ vx38))",fontsize=16,color="black",shape="box"];272 -> 298[label="",style="solid", color="black", weight=3];
731[label="vx89",fontsize=16,color="green",shape="box"];732[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];730[label="fromEnum (Char (Succ vx103)) - fromEnum (Char (Succ vx104))",fontsize=16,color="black",shape="triangle"];730 -> 735[label="",style="solid", color="black", weight=3];
733[label="digitToInt2 (Char (Succ vx98)) (True && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="black",shape="box"];733 -> 736[label="",style="solid", color="black", weight=3];
734[label="digitToInt2 (Char (Succ vx98)) (False && Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="black",shape="box"];734 -> 737[label="",style="solid", color="black", weight=3];
298[label="digitToInt1 (Char Zero) (not (primCmpNat Zero (Succ vx37) == LT) && Char Zero <= Char (Succ vx38))",fontsize=16,color="black",shape="box"];298 -> 314[label="",style="solid", color="black", weight=3];
735[label="primMinusInt (fromEnum (Char (Succ vx103))) (fromEnum (Char (Succ vx104)))",fontsize=16,color="black",shape="box"];735 -> 738[label="",style="solid", color="black", weight=3];
736[label="digitToInt2 (Char (Succ vx98)) (Char (Succ vx98) <= Char (Succ vx101))",fontsize=16,color="black",shape="box"];736 -> 739[label="",style="solid", color="black", weight=3];
737[label="digitToInt2 (Char (Succ vx98)) False",fontsize=16,color="black",shape="triangle"];737 -> 740[label="",style="solid", color="black", weight=3];
314[label="digitToInt1 (Char Zero) (not (LT == LT) && Char Zero <= Char (Succ vx38))",fontsize=16,color="black",shape="box"];314 -> 327[label="",style="solid", color="black", weight=3];
738[label="primMinusInt (primCharToInt (Char (Succ vx103))) (fromEnum (Char (Succ vx104)))",fontsize=16,color="black",shape="box"];738 -> 741[label="",style="solid", color="black", weight=3];
739[label="digitToInt2 (Char (Succ vx98)) (compare (Char (Succ vx98)) (Char (Succ vx101)) /= GT)",fontsize=16,color="black",shape="box"];739 -> 742[label="",style="solid", color="black", weight=3];
740 -> 748[label="",style="dashed", color="red", weight=0];
740[label="digitToInt1 (Char (Succ vx98)) (Char (Succ vx98) >= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) && Char (Succ vx98) <= Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];740 -> 749[label="",style="dashed", color="magenta", weight=3];
740 -> 750[label="",style="dashed", color="magenta", weight=3];
740 -> 751[label="",style="dashed", color="magenta", weight=3];
327[label="digitToInt1 (Char Zero) (not True && Char Zero <= Char (Succ vx38))",fontsize=16,color="black",shape="box"];327 -> 363[label="",style="solid", color="black", weight=3];
741[label="primMinusInt (Pos (Succ vx103)) (fromEnum (Char (Succ vx104)))",fontsize=16,color="black",shape="box"];741 -> 746[label="",style="solid", color="black", weight=3];
742[label="digitToInt2 (Char (Succ vx98)) (not (compare (Char (Succ vx98)) (Char (Succ vx101)) == GT))",fontsize=16,color="black",shape="box"];742 -> 747[label="",style="solid", color="black", weight=3];
749[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];750[label="vx98",fontsize=16,color="green",shape="box"];751[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];748[label="digitToInt1 (Char (Succ vx109)) (Char (Succ vx109) >= Char (Succ vx110) && Char (Succ vx109) <= Char (Succ vx111))",fontsize=16,color="black",shape="triangle"];748 -> 755[label="",style="solid", color="black", weight=3];
363[label="digitToInt1 (Char Zero) (False && Char Zero <= Char (Succ vx38))",fontsize=16,color="black",shape="box"];363 -> 368[label="",style="solid", color="black", weight=3];
746[label="primMinusInt (Pos (Succ vx103)) (primCharToInt (Char (Succ vx104)))",fontsize=16,color="black",shape="box"];746 -> 756[label="",style="solid", color="black", weight=3];
747[label="digitToInt2 (Char (Succ vx98)) (not (primCmpChar (Char (Succ vx98)) (Char (Succ vx101)) == GT))",fontsize=16,color="black",shape="box"];747 -> 757[label="",style="solid", color="black", weight=3];
755[label="digitToInt1 (Char (Succ vx109)) (compare (Char (Succ vx109)) (Char (Succ vx110)) /= LT && Char (Succ vx109) <= Char (Succ vx111))",fontsize=16,color="black",shape="box"];755 -> 758[label="",style="solid", color="black", weight=3];
368[label="digitToInt1 (Char Zero) False",fontsize=16,color="black",shape="box"];368 -> 373[label="",style="solid", color="black", weight=3];
756[label="primMinusInt (Pos (Succ vx103)) (Pos (Succ vx104))",fontsize=16,color="black",shape="box"];756 -> 759[label="",style="solid", color="black", weight=3];
757 -> 976[label="",style="dashed", color="red", weight=0];
757[label="digitToInt2 (Char (Succ vx98)) (not (primCmpNat (Succ vx98) (Succ vx101) == GT))",fontsize=16,color="magenta"];757 -> 977[label="",style="dashed", color="magenta", weight=3];
757 -> 978[label="",style="dashed", color="magenta", weight=3];
757 -> 979[label="",style="dashed", color="magenta", weight=3];
758[label="digitToInt1 (Char (Succ vx109)) (not (compare (Char (Succ vx109)) (Char (Succ vx110)) == LT) && Char (Succ vx109) <= Char (Succ vx111))",fontsize=16,color="black",shape="box"];758 -> 761[label="",style="solid", color="black", weight=3];
373[label="digitToInt0 (Char Zero) otherwise",fontsize=16,color="black",shape="box"];373 -> 379[label="",style="solid", color="black", weight=3];
759[label="primMinusNat (Succ vx103) (Succ vx104)",fontsize=16,color="black",shape="box"];759 -> 762[label="",style="solid", color="black", weight=3];
977[label="vx98",fontsize=16,color="green",shape="box"];978[label="Succ vx101",fontsize=16,color="green",shape="box"];979[label="Succ vx98",fontsize=16,color="green",shape="box"];976[label="digitToInt2 (Char (Succ vx119)) (not (primCmpNat vx120 vx121 == GT))",fontsize=16,color="burlywood",shape="triangle"];1306[label="vx120/Succ vx1200",fontsize=10,color="white",style="solid",shape="box"];976 -> 1306[label="",style="solid", color="burlywood", weight=9];
1306 -> 998[label="",style="solid", color="burlywood", weight=3];
1307[label="vx120/Zero",fontsize=10,color="white",style="solid",shape="box"];976 -> 1307[label="",style="solid", color="burlywood", weight=9];
1307 -> 999[label="",style="solid", color="burlywood", weight=3];
761[label="digitToInt1 (Char (Succ vx109)) (not (primCmpChar (Char (Succ vx109)) (Char (Succ vx110)) == LT) && Char (Succ vx109) <= Char (Succ vx111))",fontsize=16,color="black",shape="box"];761 -> 765[label="",style="solid", color="black", weight=3];
379[label="digitToInt0 (Char Zero) True",fontsize=16,color="black",shape="box"];379 -> 382[label="",style="solid", color="black", weight=3];
762[label="primMinusNat vx103 vx104",fontsize=16,color="burlywood",shape="triangle"];1308[label="vx103/Succ vx1030",fontsize=10,color="white",style="solid",shape="box"];762 -> 1308[label="",style="solid", color="burlywood", weight=9];
1308 -> 766[label="",style="solid", color="burlywood", weight=3];
1309[label="vx103/Zero",fontsize=10,color="white",style="solid",shape="box"];762 -> 1309[label="",style="solid", color="burlywood", weight=9];
1309 -> 767[label="",style="solid", color="burlywood", weight=3];
998[label="digitToInt2 (Char (Succ vx119)) (not (primCmpNat (Succ vx1200) vx121 == GT))",fontsize=16,color="burlywood",shape="box"];1310[label="vx121/Succ vx1210",fontsize=10,color="white",style="solid",shape="box"];998 -> 1310[label="",style="solid", color="burlywood", weight=9];
1310 -> 1012[label="",style="solid", color="burlywood", weight=3];
1311[label="vx121/Zero",fontsize=10,color="white",style="solid",shape="box"];998 -> 1311[label="",style="solid", color="burlywood", weight=9];
1311 -> 1013[label="",style="solid", color="burlywood", weight=3];
999[label="digitToInt2 (Char (Succ vx119)) (not (primCmpNat Zero vx121 == GT))",fontsize=16,color="burlywood",shape="box"];1312[label="vx121/Succ vx1210",fontsize=10,color="white",style="solid",shape="box"];999 -> 1312[label="",style="solid", color="burlywood", weight=9];
1312 -> 1014[label="",style="solid", color="burlywood", weight=3];
1313[label="vx121/Zero",fontsize=10,color="white",style="solid",shape="box"];999 -> 1313[label="",style="solid", color="burlywood", weight=9];
1313 -> 1015[label="",style="solid", color="burlywood", weight=3];
765 -> 1032[label="",style="dashed", color="red", weight=0];
765[label="digitToInt1 (Char (Succ vx109)) (not (primCmpNat (Succ vx109) (Succ vx110) == LT) && Char (Succ vx109) <= Char (Succ vx111))",fontsize=16,color="magenta"];765 -> 1033[label="",style="dashed", color="magenta", weight=3];
765 -> 1034[label="",style="dashed", color="magenta", weight=3];
765 -> 1035[label="",style="dashed", color="magenta", weight=3];
765 -> 1036[label="",style="dashed", color="magenta", weight=3];
382[label="error []",fontsize=16,color="black",shape="triangle"];382 -> 385[label="",style="solid", color="black", weight=3];
766[label="primMinusNat (Succ vx1030) vx104",fontsize=16,color="burlywood",shape="box"];1315[label="vx104/Succ vx1040",fontsize=10,color="white",style="solid",shape="box"];766 -> 1315[label="",style="solid", color="burlywood", weight=9];
1315 -> 773[label="",style="solid", color="burlywood", weight=3];
1316[label="vx104/Zero",fontsize=10,color="white",style="solid",shape="box"];766 -> 1316[label="",style="solid", color="burlywood", weight=9];
1316 -> 774[label="",style="solid", color="burlywood", weight=3];
767[label="primMinusNat Zero vx104",fontsize=16,color="burlywood",shape="box"];1317[label="vx104/Succ vx1040",fontsize=10,color="white",style="solid",shape="box"];767 -> 1317[label="",style="solid", color="burlywood", weight=9];
1317 -> 775[label="",style="solid", color="burlywood", weight=3];
1318[label="vx104/Zero",fontsize=10,color="white",style="solid",shape="box"];767 -> 1318[label="",style="solid", color="burlywood", weight=9];
1318 -> 776[label="",style="solid", color="burlywood", weight=3];
1012[label="digitToInt2 (Char (Succ vx119)) (not (primCmpNat (Succ vx1200) (Succ vx1210) == GT))",fontsize=16,color="black",shape="box"];1012 -> 1028[label="",style="solid", color="black", weight=3];
1013[label="digitToInt2 (Char (Succ vx119)) (not (primCmpNat (Succ vx1200) Zero == GT))",fontsize=16,color="black",shape="box"];1013 -> 1029[label="",style="solid", color="black", weight=3];
1014[label="digitToInt2 (Char (Succ vx119)) (not (primCmpNat Zero (Succ vx1210) == GT))",fontsize=16,color="black",shape="box"];1014 -> 1030[label="",style="solid", color="black", weight=3];
1015[label="digitToInt2 (Char (Succ vx119)) (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];1015 -> 1031[label="",style="solid", color="black", weight=3];
1033[label="vx109",fontsize=16,color="green",shape="box"];1034[label="vx111",fontsize=16,color="green",shape="box"];1035[label="Succ vx110",fontsize=16,color="green",shape="box"];1036[label="Succ vx109",fontsize=16,color="green",shape="box"];1032[label="digitToInt1 (Char (Succ vx123)) (not (primCmpNat vx124 vx125 == LT) && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="burlywood",shape="triangle"];1319[label="vx124/Succ vx1240",fontsize=10,color="white",style="solid",shape="box"];1032 -> 1319[label="",style="solid", color="burlywood", weight=9];
1319 -> 1061[label="",style="solid", color="burlywood", weight=3];
1320[label="vx124/Zero",fontsize=10,color="white",style="solid",shape="box"];1032 -> 1320[label="",style="solid", color="burlywood", weight=9];
1320 -> 1062[label="",style="solid", color="burlywood", weight=3];
385[label="error []",fontsize=16,color="red",shape="box"];773[label="primMinusNat (Succ vx1030) (Succ vx1040)",fontsize=16,color="black",shape="box"];773 -> 783[label="",style="solid", color="black", weight=3];
774[label="primMinusNat (Succ vx1030) Zero",fontsize=16,color="black",shape="box"];774 -> 784[label="",style="solid", color="black", weight=3];
775[label="primMinusNat Zero (Succ vx1040)",fontsize=16,color="black",shape="box"];775 -> 785[label="",style="solid", color="black", weight=3];
776[label="primMinusNat Zero Zero",fontsize=16,color="black",shape="box"];776 -> 786[label="",style="solid", color="black", weight=3];
1028 -> 976[label="",style="dashed", color="red", weight=0];
1028[label="digitToInt2 (Char (Succ vx119)) (not (primCmpNat vx1200 vx1210 == GT))",fontsize=16,color="magenta"];1028 -> 1063[label="",style="dashed", color="magenta", weight=3];
1028 -> 1064[label="",style="dashed", color="magenta", weight=3];
1029[label="digitToInt2 (Char (Succ vx119)) (not (GT == GT))",fontsize=16,color="black",shape="box"];1029 -> 1065[label="",style="solid", color="black", weight=3];
1030[label="digitToInt2 (Char (Succ vx119)) (not (LT == GT))",fontsize=16,color="black",shape="box"];1030 -> 1066[label="",style="solid", color="black", weight=3];
1031[label="digitToInt2 (Char (Succ vx119)) (not (EQ == GT))",fontsize=16,color="black",shape="box"];1031 -> 1067[label="",style="solid", color="black", weight=3];
1061[label="digitToInt1 (Char (Succ vx123)) (not (primCmpNat (Succ vx1240) vx125 == LT) && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="burlywood",shape="box"];1322[label="vx125/Succ vx1250",fontsize=10,color="white",style="solid",shape="box"];1061 -> 1322[label="",style="solid", color="burlywood", weight=9];
1322 -> 1068[label="",style="solid", color="burlywood", weight=3];
1323[label="vx125/Zero",fontsize=10,color="white",style="solid",shape="box"];1061 -> 1323[label="",style="solid", color="burlywood", weight=9];
1323 -> 1069[label="",style="solid", color="burlywood", weight=3];
1062[label="digitToInt1 (Char (Succ vx123)) (not (primCmpNat Zero vx125 == LT) && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="burlywood",shape="box"];1324[label="vx125/Succ vx1250",fontsize=10,color="white",style="solid",shape="box"];1062 -> 1324[label="",style="solid", color="burlywood", weight=9];
1324 -> 1070[label="",style="solid", color="burlywood", weight=3];
1325[label="vx125/Zero",fontsize=10,color="white",style="solid",shape="box"];1062 -> 1325[label="",style="solid", color="burlywood", weight=9];
1325 -> 1071[label="",style="solid", color="burlywood", weight=3];
783 -> 762[label="",style="dashed", color="red", weight=0];
783[label="primMinusNat vx1030 vx1040",fontsize=16,color="magenta"];783 -> 796[label="",style="dashed", color="magenta", weight=3];
783 -> 797[label="",style="dashed", color="magenta", weight=3];
784[label="Pos (Succ vx1030)",fontsize=16,color="green",shape="box"];785[label="Neg (Succ vx1040)",fontsize=16,color="green",shape="box"];786[label="Pos Zero",fontsize=16,color="green",shape="box"];1063[label="vx1210",fontsize=16,color="green",shape="box"];1064[label="vx1200",fontsize=16,color="green",shape="box"];1065[label="digitToInt2 (Char (Succ vx119)) (not True)",fontsize=16,color="black",shape="box"];1065 -> 1072[label="",style="solid", color="black", weight=3];
1066[label="digitToInt2 (Char (Succ vx119)) (not False)",fontsize=16,color="black",shape="triangle"];1066 -> 1073[label="",style="solid", color="black", weight=3];
1067 -> 1066[label="",style="dashed", color="red", weight=0];
1067[label="digitToInt2 (Char (Succ vx119)) (not False)",fontsize=16,color="magenta"];1068[label="digitToInt1 (Char (Succ vx123)) (not (primCmpNat (Succ vx1240) (Succ vx1250) == LT) && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="black",shape="box"];1068 -> 1074[label="",style="solid", color="black", weight=3];
1069[label="digitToInt1 (Char (Succ vx123)) (not (primCmpNat (Succ vx1240) Zero == LT) && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="black",shape="box"];1069 -> 1075[label="",style="solid", color="black", weight=3];
1070[label="digitToInt1 (Char (Succ vx123)) (not (primCmpNat Zero (Succ vx1250) == LT) && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="black",shape="box"];1070 -> 1076[label="",style="solid", color="black", weight=3];
1071[label="digitToInt1 (Char (Succ vx123)) (not (primCmpNat Zero Zero == LT) && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="black",shape="box"];1071 -> 1077[label="",style="solid", color="black", weight=3];
796[label="vx1030",fontsize=16,color="green",shape="box"];797[label="vx1040",fontsize=16,color="green",shape="box"];1072 -> 737[label="",style="dashed", color="red", weight=0];
1072[label="digitToInt2 (Char (Succ vx119)) False",fontsize=16,color="magenta"];1072 -> 1078[label="",style="dashed", color="magenta", weight=3];
1073[label="digitToInt2 (Char (Succ vx119)) True",fontsize=16,color="black",shape="box"];1073 -> 1079[label="",style="solid", color="black", weight=3];
1074 -> 1032[label="",style="dashed", color="red", weight=0];
1074[label="digitToInt1 (Char (Succ vx123)) (not (primCmpNat vx1240 vx1250 == LT) && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="magenta"];1074 -> 1080[label="",style="dashed", color="magenta", weight=3];
1074 -> 1081[label="",style="dashed", color="magenta", weight=3];
1075[label="digitToInt1 (Char (Succ vx123)) (not (GT == LT) && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="black",shape="box"];1075 -> 1082[label="",style="solid", color="black", weight=3];
1076[label="digitToInt1 (Char (Succ vx123)) (not (LT == LT) && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="black",shape="box"];1076 -> 1083[label="",style="solid", color="black", weight=3];
1077[label="digitToInt1 (Char (Succ vx123)) (not (EQ == LT) && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="black",shape="box"];1077 -> 1084[label="",style="solid", color="black", weight=3];
1078[label="vx119",fontsize=16,color="green",shape="box"];1079 -> 1097[label="",style="dashed", color="red", weight=0];
1079[label="fromEnum (Char (Succ vx119)) - fromEnum (Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))",fontsize=16,color="magenta"];1079 -> 1098[label="",style="dashed", color="magenta", weight=3];
1079 -> 1099[label="",style="dashed", color="magenta", weight=3];
1080[label="vx1250",fontsize=16,color="green",shape="box"];1081[label="vx1240",fontsize=16,color="green",shape="box"];1082[label="digitToInt1 (Char (Succ vx123)) (not False && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="black",shape="triangle"];1082 -> 1088[label="",style="solid", color="black", weight=3];
1083[label="digitToInt1 (Char (Succ vx123)) (not True && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="black",shape="box"];1083 -> 1089[label="",style="solid", color="black", weight=3];
1084 -> 1082[label="",style="dashed", color="red", weight=0];
1084[label="digitToInt1 (Char (Succ vx123)) (not False && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="magenta"];1098[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))",fontsize=16,color="green",shape="box"];1099 -> 730[label="",style="dashed", color="red", weight=0];
1099[label="fromEnum (Char (Succ vx119)) - fromEnum (Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];1099 -> 1101[label="",style="dashed", color="magenta", weight=3];
1099 -> 1102[label="",style="dashed", color="magenta", weight=3];
1097[label="vx134 + Pos (Succ vx133)",fontsize=16,color="black",shape="triangle"];1097 -> 1103[label="",style="solid", color="black", weight=3];
1088[label="digitToInt1 (Char (Succ vx123)) (True && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="black",shape="box"];1088 -> 1104[label="",style="solid", color="black", weight=3];
1089[label="digitToInt1 (Char (Succ vx123)) (False && Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="black",shape="box"];1089 -> 1105[label="",style="solid", color="black", weight=3];
1101[label="vx119",fontsize=16,color="green",shape="box"];1102[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];1103[label="primPlusInt vx134 (Pos (Succ vx133))",fontsize=16,color="burlywood",shape="box"];1333[label="vx134/Pos vx1340",fontsize=10,color="white",style="solid",shape="box"];1103 -> 1333[label="",style="solid", color="burlywood", weight=9];
1333 -> 1106[label="",style="solid", color="burlywood", weight=3];
1334[label="vx134/Neg vx1340",fontsize=10,color="white",style="solid",shape="box"];1103 -> 1334[label="",style="solid", color="burlywood", weight=9];
1334 -> 1107[label="",style="solid", color="burlywood", weight=3];
1104[label="digitToInt1 (Char (Succ vx123)) (Char (Succ vx123) <= Char (Succ vx126))",fontsize=16,color="black",shape="box"];1104 -> 1108[label="",style="solid", color="black", weight=3];
1105[label="digitToInt1 (Char (Succ vx123)) False",fontsize=16,color="black",shape="triangle"];1105 -> 1109[label="",style="solid", color="black", weight=3];
1106[label="primPlusInt (Pos vx1340) (Pos (Succ vx133))",fontsize=16,color="black",shape="box"];1106 -> 1110[label="",style="solid", color="black", weight=3];
1107[label="primPlusInt (Neg vx1340) (Pos (Succ vx133))",fontsize=16,color="black",shape="box"];1107 -> 1111[label="",style="solid", color="black", weight=3];
1108[label="digitToInt1 (Char (Succ vx123)) (compare (Char (Succ vx123)) (Char (Succ vx126)) /= GT)",fontsize=16,color="black",shape="box"];1108 -> 1112[label="",style="solid", color="black", weight=3];
1109[label="digitToInt0 (Char (Succ vx123)) otherwise",fontsize=16,color="black",shape="box"];1109 -> 1113[label="",style="solid", color="black", weight=3];
1110[label="Pos (primPlusNat vx1340 (Succ vx133))",fontsize=16,color="green",shape="box"];1110 -> 1114[label="",style="dashed", color="green", weight=3];
1111 -> 762[label="",style="dashed", color="red", weight=0];
1111[label="primMinusNat (Succ vx133) vx1340",fontsize=16,color="magenta"];1111 -> 1115[label="",style="dashed", color="magenta", weight=3];
1111 -> 1116[label="",style="dashed", color="magenta", weight=3];
1112[label="digitToInt1 (Char (Succ vx123)) (not (compare (Char (Succ vx123)) (Char (Succ vx126)) == GT))",fontsize=16,color="black",shape="box"];1112 -> 1117[label="",style="solid", color="black", weight=3];
1113[label="digitToInt0 (Char (Succ vx123)) True",fontsize=16,color="black",shape="box"];1113 -> 1118[label="",style="solid", color="black", weight=3];
1114[label="primPlusNat vx1340 (Succ vx133)",fontsize=16,color="burlywood",shape="box"];1336[label="vx1340/Succ vx13400",fontsize=10,color="white",style="solid",shape="box"];1114 -> 1336[label="",style="solid", color="burlywood", weight=9];
1336 -> 1119[label="",style="solid", color="burlywood", weight=3];
1337[label="vx1340/Zero",fontsize=10,color="white",style="solid",shape="box"];1114 -> 1337[label="",style="solid", color="burlywood", weight=9];
1337 -> 1120[label="",style="solid", color="burlywood", weight=3];
1115[label="Succ vx133",fontsize=16,color="green",shape="box"];1116[label="vx1340",fontsize=16,color="green",shape="box"];1117[label="digitToInt1 (Char (Succ vx123)) (not (primCmpChar (Char (Succ vx123)) (Char (Succ vx126)) == GT))",fontsize=16,color="black",shape="box"];1117 -> 1121[label="",style="solid", color="black", weight=3];
1118 -> 382[label="",style="dashed", color="red", weight=0];
1118[label="error []",fontsize=16,color="magenta"];1119[label="primPlusNat (Succ vx13400) (Succ vx133)",fontsize=16,color="black",shape="box"];1119 -> 1122[label="",style="solid", color="black", weight=3];
1120[label="primPlusNat Zero (Succ vx133)",fontsize=16,color="black",shape="box"];1120 -> 1123[label="",style="solid", color="black", weight=3];
1121 -> 1223[label="",style="dashed", color="red", weight=0];
1121[label="digitToInt1 (Char (Succ vx123)) (not (primCmpNat (Succ vx123) (Succ vx126) == GT))",fontsize=16,color="magenta"];1121 -> 1224[label="",style="dashed", color="magenta", weight=3];
1121 -> 1225[label="",style="dashed", color="magenta", weight=3];
1121 -> 1226[label="",style="dashed", color="magenta", weight=3];
1122[label="Succ (Succ (primPlusNat vx13400 vx133))",fontsize=16,color="green",shape="box"];1122 -> 1125[label="",style="dashed", color="green", weight=3];
1123[label="Succ vx133",fontsize=16,color="green",shape="box"];1224[label="Succ vx123",fontsize=16,color="green",shape="box"];1225[label="Succ vx126",fontsize=16,color="green",shape="box"];1226[label="vx123",fontsize=16,color="green",shape="box"];1223[label="digitToInt1 (Char (Succ vx136)) (not (primCmpNat vx137 vx138 == GT))",fontsize=16,color="burlywood",shape="triangle"];1340[label="vx137/Succ vx1370",fontsize=10,color="white",style="solid",shape="box"];1223 -> 1340[label="",style="solid", color="burlywood", weight=9];
1340 -> 1245[label="",style="solid", color="burlywood", weight=3];
1341[label="vx137/Zero",fontsize=10,color="white",style="solid",shape="box"];1223 -> 1341[label="",style="solid", color="burlywood", weight=9];
1341 -> 1246[label="",style="solid", color="burlywood", weight=3];
1125[label="primPlusNat vx13400 vx133",fontsize=16,color="burlywood",shape="triangle"];1342[label="vx13400/Succ vx134000",fontsize=10,color="white",style="solid",shape="box"];1125 -> 1342[label="",style="solid", color="burlywood", weight=9];
1342 -> 1128[label="",style="solid", color="burlywood", weight=3];
1343[label="vx13400/Zero",fontsize=10,color="white",style="solid",shape="box"];1125 -> 1343[label="",style="solid", color="burlywood", weight=9];
1343 -> 1129[label="",style="solid", color="burlywood", weight=3];
1245[label="digitToInt1 (Char (Succ vx136)) (not (primCmpNat (Succ vx1370) vx138 == GT))",fontsize=16,color="burlywood",shape="box"];1344[label="vx138/Succ vx1380",fontsize=10,color="white",style="solid",shape="box"];1245 -> 1344[label="",style="solid", color="burlywood", weight=9];
1344 -> 1247[label="",style="solid", color="burlywood", weight=3];
1345[label="vx138/Zero",fontsize=10,color="white",style="solid",shape="box"];1245 -> 1345[label="",style="solid", color="burlywood", weight=9];
1345 -> 1248[label="",style="solid", color="burlywood", weight=3];
1246[label="digitToInt1 (Char (Succ vx136)) (not (primCmpNat Zero vx138 == GT))",fontsize=16,color="burlywood",shape="box"];1346[label="vx138/Succ vx1380",fontsize=10,color="white",style="solid",shape="box"];1246 -> 1346[label="",style="solid", color="burlywood", weight=9];
1346 -> 1249[label="",style="solid", color="burlywood", weight=3];
1347[label="vx138/Zero",fontsize=10,color="white",style="solid",shape="box"];1246 -> 1347[label="",style="solid", color="burlywood", weight=9];
1347 -> 1250[label="",style="solid", color="burlywood", weight=3];
1128[label="primPlusNat (Succ vx134000) vx133",fontsize=16,color="burlywood",shape="box"];1348[label="vx133/Succ vx1330",fontsize=10,color="white",style="solid",shape="box"];1128 -> 1348[label="",style="solid", color="burlywood", weight=9];
1348 -> 1134[label="",style="solid", color="burlywood", weight=3];
1349[label="vx133/Zero",fontsize=10,color="white",style="solid",shape="box"];1128 -> 1349[label="",style="solid", color="burlywood", weight=9];
1349 -> 1135[label="",style="solid", color="burlywood", weight=3];
1129[label="primPlusNat Zero vx133",fontsize=16,color="burlywood",shape="box"];1350[label="vx133/Succ vx1330",fontsize=10,color="white",style="solid",shape="box"];1129 -> 1350[label="",style="solid", color="burlywood", weight=9];
1350 -> 1136[label="",style="solid", color="burlywood", weight=3];
1351[label="vx133/Zero",fontsize=10,color="white",style="solid",shape="box"];1129 -> 1351[label="",style="solid", color="burlywood", weight=9];
1351 -> 1137[label="",style="solid", color="burlywood", weight=3];
1247[label="digitToInt1 (Char (Succ vx136)) (not (primCmpNat (Succ vx1370) (Succ vx1380) == GT))",fontsize=16,color="black",shape="box"];1247 -> 1251[label="",style="solid", color="black", weight=3];
1248[label="digitToInt1 (Char (Succ vx136)) (not (primCmpNat (Succ vx1370) Zero == GT))",fontsize=16,color="black",shape="box"];1248 -> 1252[label="",style="solid", color="black", weight=3];
1249[label="digitToInt1 (Char (Succ vx136)) (not (primCmpNat Zero (Succ vx1380) == GT))",fontsize=16,color="black",shape="box"];1249 -> 1253[label="",style="solid", color="black", weight=3];
1250[label="digitToInt1 (Char (Succ vx136)) (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];1250 -> 1254[label="",style="solid", color="black", weight=3];
1134[label="primPlusNat (Succ vx134000) (Succ vx1330)",fontsize=16,color="black",shape="box"];1134 -> 1142[label="",style="solid", color="black", weight=3];
1135[label="primPlusNat (Succ vx134000) Zero",fontsize=16,color="black",shape="box"];1135 -> 1143[label="",style="solid", color="black", weight=3];
1136[label="primPlusNat Zero (Succ vx1330)",fontsize=16,color="black",shape="box"];1136 -> 1144[label="",style="solid", color="black", weight=3];
1137[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];1137 -> 1145[label="",style="solid", color="black", weight=3];
1251 -> 1223[label="",style="dashed", color="red", weight=0];
1251[label="digitToInt1 (Char (Succ vx136)) (not (primCmpNat vx1370 vx1380 == GT))",fontsize=16,color="magenta"];1251 -> 1255[label="",style="dashed", color="magenta", weight=3];
1251 -> 1256[label="",style="dashed", color="magenta", weight=3];
1252[label="digitToInt1 (Char (Succ vx136)) (not (GT == GT))",fontsize=16,color="black",shape="box"];1252 -> 1257[label="",style="solid", color="black", weight=3];
1253[label="digitToInt1 (Char (Succ vx136)) (not (LT == GT))",fontsize=16,color="black",shape="box"];1253 -> 1258[label="",style="solid", color="black", weight=3];
1254[label="digitToInt1 (Char (Succ vx136)) (not (EQ == GT))",fontsize=16,color="black",shape="box"];1254 -> 1259[label="",style="solid", color="black", weight=3];
1142[label="Succ (Succ (primPlusNat vx134000 vx1330))",fontsize=16,color="green",shape="box"];1142 -> 1151[label="",style="dashed", color="green", weight=3];
1143[label="Succ vx134000",fontsize=16,color="green",shape="box"];1144[label="Succ vx1330",fontsize=16,color="green",shape="box"];1145[label="Zero",fontsize=16,color="green",shape="box"];1255[label="vx1370",fontsize=16,color="green",shape="box"];1256[label="vx1380",fontsize=16,color="green",shape="box"];1257[label="digitToInt1 (Char (Succ vx136)) (not True)",fontsize=16,color="black",shape="box"];1257 -> 1260[label="",style="solid", color="black", weight=3];
1258[label="digitToInt1 (Char (Succ vx136)) (not False)",fontsize=16,color="black",shape="triangle"];1258 -> 1261[label="",style="solid", color="black", weight=3];
1259 -> 1258[label="",style="dashed", color="red", weight=0];
1259[label="digitToInt1 (Char (Succ vx136)) (not False)",fontsize=16,color="magenta"];1151 -> 1125[label="",style="dashed", color="red", weight=0];
1151[label="primPlusNat vx134000 vx1330",fontsize=16,color="magenta"];1151 -> 1158[label="",style="dashed", color="magenta", weight=3];
1151 -> 1159[label="",style="dashed", color="magenta", weight=3];
1260 -> 1105[label="",style="dashed", color="red", weight=0];
1260[label="digitToInt1 (Char (Succ vx136)) False",fontsize=16,color="magenta"];1260 -> 1262[label="",style="dashed", color="magenta", weight=3];
1261[label="digitToInt1 (Char (Succ vx136)) True",fontsize=16,color="black",shape="box"];1261 -> 1263[label="",style="solid", color="black", weight=3];
1158[label="vx1330",fontsize=16,color="green",shape="box"];1159[label="vx134000",fontsize=16,color="green",shape="box"];1262[label="vx136",fontsize=16,color="green",shape="box"];1263 -> 1097[label="",style="dashed", color="red", weight=0];
1263[label="fromEnum (Char (Succ vx136)) - fromEnum (Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))",fontsize=16,color="magenta"];1263 -> 1264[label="",style="dashed", color="magenta", weight=3];
1263 -> 1265[label="",style="dashed", color="magenta", weight=3];
1264[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))",fontsize=16,color="green",shape="box"];1265 -> 730[label="",style="dashed", color="red", weight=0];
1265[label="fromEnum (Char (Succ vx136)) - fromEnum (Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="magenta"];1265 -> 1266[label="",style="dashed", color="magenta", weight=3];
1265 -> 1267[label="",style="dashed", color="magenta", weight=3];
1266[label="vx136",fontsize=16,color="green",shape="box"];1267[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMinusNat(Succ(vx1030), Succ(vx1040)) → new_primMinusNat(vx1030, vx1040)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primMinusNat(Succ(vx1030), Succ(vx1040)) → new_primMinusNat(vx1030, vx1040)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vx134000), Succ(vx1330)) → new_primPlusNat(vx134000, vx1330)

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(vx134000), Succ(vx1330)) → new_primPlusNat(vx134000, vx1330)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_digitToInt1(vx136, Succ(vx1370), Succ(vx1380)) → new_digitToInt1(vx136, vx1370, vx1380)

From the DPs we obtained the following set of size-change graphs:

new_digitToInt1(vx136, Succ(vx1370), Succ(vx1380)) → new_digitToInt1(vx136, vx1370, vx1380)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_digitToInt10(vx123, Succ(vx1240), Succ(vx1250), vx126) → new_digitToInt10(vx123, vx1240, vx1250, vx126)

From the DPs we obtained the following set of size-change graphs:

new_digitToInt10(vx123, Succ(vx1240), Succ(vx1250), vx126) → new_digitToInt10(vx123, vx1240, vx1250, vx126)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_digitToInt2(vx119, Succ(vx1200), Succ(vx1210)) → new_digitToInt2(vx119, vx1200, vx1210)

From the DPs we obtained the following set of size-change graphs:

new_digitToInt2(vx119, Succ(vx1200), Succ(vx1210)) → new_digitToInt2(vx119, vx1200, vx1210)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_digitToInt20(vx98, Succ(vx990), Succ(vx1000), vx101) → new_digitToInt20(vx98, vx990, vx1000, vx101)

From the DPs we obtained the following set of size-change graphs:

new_digitToInt20(vx98, Succ(vx990), Succ(vx1000), vx101) → new_digitToInt20(vx98, vx990, vx1000, vx101)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_digitToInt3(vx89, Succ(vx900), Succ(vx910)) → new_digitToInt3(vx89, vx900, vx910)

From the DPs we obtained the following set of size-change graphs:

new_digitToInt3(vx89, Succ(vx900), Succ(vx910)) → new_digitToInt3(vx89, vx900, vx910)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_digitToInt30(vx61, Succ(vx620), Succ(vx630), vx64) → new_digitToInt30(vx61, vx620, vx630, vx64)

From the DPs we obtained the following set of size-change graphs:

new_digitToInt30(vx61, Succ(vx620), Succ(vx630), vx64) → new_digitToInt30(vx61, vx620, vx630, vx64)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4

digitToInt1	c True	= fromEnum c - fromEnum 'A' + 10
digitToInt1	c False	= digitToInt0 c otherwise

digitToInt3	c True	= fromEnum c - fromEnum '0'
digitToInt3	c False	= digitToInt2 c (c >= 'a' && c <= 'f')

digitToInt2	c True	= fromEnum c - fromEnum 'a' + 10
digitToInt2	c False	= digitToInt1 c (c >= 'A' && c <= 'F')